Lemmas | es realizer-induction, Id wf, R-Feasible wf, fpf wf, R-state wf, R-Dsys wf, msga wf, es realizer wf, fpf-empty wf, Rnone wf, eq id wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, fpf-single wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, Rinit wf, Rframe wf, Knd wf, lsrc wf, Rsframe wf, IdLnk wf, Reffect wf, decl-state wf, decl-type wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, Rrframe wf, fpf-join wf, squash wf, true wf, deq wf, id-deq wf |